#include <typeinfo>
#include <string>
#include <stdio.h>
#include <stdlib.h>
#include "smt.h"
#include <iostream>
#include "cfa.h"
using namespace std;

extern bool CompareExpr(Expr*, Expr*);
extern string Int2String(int y);

void display(yicesl_context ctx) {
  if (yicesl_inconsistent(ctx))
    printf("unsatisfiable\n");
  else
    printf("satisfiable\n");
}
void testyices1(){
    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    yicesl_read(ctx, "(define x::int)");
    yicesl_read(ctx, "(define y::int)");
    yicesl_read(ctx, "(assert (= (+ x y) 0))");
    yicesl_read(ctx, "(assert (>= y 0))");
    display(ctx);
    yicesl_read(ctx, "(push)");
    yicesl_read(ctx, "(assert (>= x 1))");
    display(ctx);
    yicesl_read(ctx, "(pop)");
    yicesl_read(ctx, "(assert (>= x 0))");
    display(ctx);
    yicesl_read(ctx, "(set-evidence! true)");
    yicesl_read(ctx, "(check)");
    yicesl_del_context(ctx);   
}
void testyices(){
    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    yicesl_read(ctx, "(define x::int)");
    yicesl_read(ctx, "(define f::(-> int int))");
    //yicesl_read(ctx, "(define f1::(-> int int))");
    //yicesl_read(ctx, "(define f2::(-> int int))");
    yicesl_read(ctx, "(assert(= x 5))");
    //yicesl_read(ctx, "(assert(update f (0) 10)");
    //yicesl_read(ctx, "(assert(= f2 (update f1 (0) 1)))");
    //yicesl_read(ctx, "(assert(/= (f2 0) 2))");
    yicesl_read(ctx, "(assert(= (f 0) 10))");
    yicesl_read(ctx, "(assert(= (f (- x 5)) 1))");
    yicesl_read(ctx, "(check)");
    display(ctx);
}
/*int exp(int x, int t){
    int i1, i2;
    i2 = 1;
    for(i1 = 0; i1 < t; i1++){
        i2 = i2 * x;
    }
    return i2;
}
string Int2String(int y){
    string r;
    r.clear();
    int i, i1, i2, x, z;
    z = y;
    if(y < 0){ x = (-1)*y; y = (-1)*y; }
    else{ x= y; }
    if(y == 0){ return "0"; }
    for(i1 = 0; y > 0; y = y/10){
        i1 = i1 + 1;
    }
    for(; i1 > 0; i1--){
        i2 = x / exp(10, i1-1);
        x = x % exp(10, i1-1);
        r = r + (char)(i2+48);
    }
    if(z< 0){ r = "-" + r; }
    return r;
}*/
int NumLine(int x){
    int i1 = 0;
    for(i1 = 0; x > 0; x = x/10){
        i1 = i1 + 1;
    }
    return i1;
}
char ChangeSymbolOP(OPType op){
    if(op == Plus){ return '+'; }
    else if(op == Minus){ return '-'; }
    else if(op == Multi){ return '*'; }
    else if(op == Divide){ return '/'; }
    else{ return 'X';}
}
char* ChangeSymbolLT(LogicType l){
    if(l == And){ return "and"; }
    else{ return "or"; }
}
char* ChangeSymbolPT(PropType p){
    if(p == LT){ return "<"; }
    else if(p == GT){ return ">"; }
    else{ return "="; }
}
string RecursiveSMTExpr(Expr* E, yicesl_context *ctx, vector<Expr*> *VE){
    int Flag;
    string s, n;
    //char c[33];
    if(typeid(*E) == typeid(IntExpr)){
        //itoa(((IntExpr*)E)->i, c, 10);
        s = Int2String(((IntExpr*)E)->i);
    }
    else if(typeid(*E) == typeid(SelectExpr)){
        s = ((VarExpr*)(((SelectExpr*)E)->a))->x; s = s + '[';
        s = s + RecursiveSMTExpr(((SelectExpr*)E)->i, ctx, VE);
        s = s + ']';
    }
    else if(typeid(*E) == typeid(VarExpr)){
        s = ((VarExpr*)E)->x;
        //cout << "E->name = " << ((VarExpr*)E)->s << " size = " << VE->size() << endl;
        Flag = -1;
        for(int i1 = 0; i1 < (int)VE->size(); i1++){
            if(CompareExpr((*VE)[i1], E)){
                Flag = 1;
            }
        }
        if(Flag == -1){
            VE->push_back(E);
            n = ((VarExpr*)E)->x;
            n = "(define " + n + "::int)";
            //cout << "n = " << n << endl;
            yicesl_read((*ctx), (char*)(n.c_str()));
        }
    }
    else if(typeid(*E) == typeid(BinExpr)){
        s = ChangeSymbolOP(((BinExpr*)E)->op);
        if(typeid(*(((BinExpr*)E)->e1)) == typeid(BinExpr) && typeid(*(((BinExpr*)E)->e2)) != typeid(BinExpr)){
            s = s + " ( " + RecursiveSMTExpr(((BinExpr*)E)->e1, ctx, VE) + " ) " + RecursiveSMTExpr(((BinExpr*)E)->e2, ctx, VE);
        }
        else if(typeid(*(((BinExpr*)E)->e2)) == typeid(BinExpr) && typeid(*(((BinExpr*)E)->e1)) != typeid(BinExpr)){
            s = s + " " + RecursiveSMTExpr(((BinExpr*)E)->e1, ctx, VE) + " ( " + RecursiveSMTExpr(((BinExpr*)E)->e2, ctx, VE) + " )";
        }
        else if(typeid(*(((BinExpr*)E)->e1)) == typeid(BinExpr) && typeid(*(((BinExpr*)E)->e2)) == typeid(BinExpr)){
            s = s + " ( " + RecursiveSMTExpr(((BinExpr*)E)->e1, ctx, VE) + " ) ( " + RecursiveSMTExpr(((BinExpr*)E)->e2, ctx, VE) + " )";
        }
        else{
            s = s + " " + RecursiveSMTExpr(((BinExpr*)E)->e1, ctx, VE) + " " + RecursiveSMTExpr(((BinExpr*)E)->e2, ctx, VE);
        }
    }
    else{
    }
    return s;
}
string RecursiveSMTProp(Prop* P, yicesl_context *ctx,  vector<Expr*>* E){
    string s, s1, s2;
    if(typeid(*P) == typeid(BoolProp)){
        if(((BoolProp*)P)->b == true){ s = " true "; }
        else{ s = " false "; }
    }
    else if(typeid(*P) == typeid(NegProp)){
        s  = "not";
        s1 = RecursiveSMTProp(((NegProp*)P)->p, ctx, E);
        s  = "( " + s + " " + s1 + " )";
    }
    else if(typeid(*P) == typeid(BinProp)){
        s = ChangeSymbolLT(((BinProp*)P)->l);
        s1 = RecursiveSMTProp(((BinProp*)P)->p1, ctx, E);
        /*if(typeid(*(((BinProp*)P)->p1)) == typeid(BinProp)){
            s1 = "(" + s1 + ")";
        }else{ }*/
        s2 = RecursiveSMTProp(((BinProp*)P)->p2, ctx, E);
        /*if(typeid(*(((BinProp*)P)->p2)) == typeid(BinProp)){
            s2 = "(" + s2 + ")";
        }else{ }*/
        s = "( " + s + " " + s1 + " " + s2 + " )";
    }
    else if(typeid(*P) == typeid(InequProp)){
        s = ChangeSymbolPT(((InequProp*)P)->p);
        s1 = RecursiveSMTExpr(((InequProp*)P)->e1, ctx, E);
        if(typeid(*(((InequProp*)P)->e1)) == typeid(BinExpr)){ s1 = "( " + s1 + " )"; }
        s2 = RecursiveSMTExpr(((InequProp*)P)->e2, ctx, E);
        if(typeid(*(((InequProp*)P)->e2)) == typeid(BinExpr)){ s2 = "( " + s2 + " )"; }
        s = "( " + s + " " + s1 + " " + s2 + " )";
    }
    else{
    }
    return s;
}
bool interfaceSMT(Prop* v){
    string s, s1, s2;
    vector<Expr*> E;
    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    s.clear(); s1.clear(); s2.clear();
    if(typeid(*v) == typeid(BoolProp)){
        if(((BoolProp*)v)->b == true){ s = "( assert true )"; }
        else{ s = "( assert false )"; }
        yicesl_read(ctx, (char*)(s.c_str()));
    }
    else if(typeid(*v) == typeid(NegProp)){
        s = "not";
        s1 = RecursiveSMTProp(((NegProp*)v)->p, &ctx, &E);
        s = "( " + s + " " + s1 + " )";
        s = "( assert" + s + " )";
        yicesl_read(ctx, (char*)(s.c_str()));
    }
    else if(typeid(*v) == typeid(BinProp)){
        s = ChangeSymbolLT(((BinProp*)v)->l);
        s1 = RecursiveSMTProp(((BinProp*)v)->p1, &ctx, &E);
        /*if(typeid(*(((BinProp*)v)->p1)) == typeid(BinProp)){
            s1 = "(" + s1 + ")";
        }else{ }*/
        s2 = RecursiveSMTProp(((BinProp*)v)->p2, &ctx, &E);
        /*if(typeid(*(((BinProp*)v)->p2)) == typeid(BinProp)){
            s2 = "(" + s2 + ")";
        }else{ }*/
        s = "( " + s + " " + s1 + " " + s2 + " )";
        s = "( assert" + s + " )";
        //s = "(assert" + s1 + ")";
        //cout << "s= " << s << endl;
        //yicesl_read(ctx, (char*)(s.c_str()));
        //s = "(assert" + s2 + ")";
        yicesl_read(ctx, (char*)(s.c_str()));
    }
    else if(typeid(*v) == typeid(InequProp)){
        s = ChangeSymbolPT(((InequProp*)v)->p);
        s1 = RecursiveSMTExpr(((InequProp*)v)->e1, &ctx, &E);
        if(typeid(*(((InequProp*)v)->e1)) == typeid(BinExpr)){ s1 = "( " + s1 + " )"; }
        s2 = RecursiveSMTExpr(((InequProp*)v)->e2, &ctx, &E);
        if(typeid(*(((InequProp*)v)->e2)) == typeid(BinExpr)){ s2 = "( " + s2 + " )"; }
        s = "( " + s + " " + s1 + " " + s2 + " )";
        s = "( assert(" + s + ") )";
        yicesl_read(ctx, (char*)(s.c_str()));
    }
    //yicesl_read(ctx, "(assert( < (x) (1) )");
    //yicesl_read(ctx, "(assert( < (y) (1) )");

    //cout << "s = " << s << endl;
    return yicesl_inconsistent(ctx);
}
bool testyicesinterface(){
    CFA cfa;
    Prop *P, *Q, *R1, *R2, *S1, *S2, *S3;
    P = new BinProp;
    ((BinProp*)P)->p1 = new InequProp;
    ((BinProp*)P)->p2 = new InequProp;
    ((BinProp*)P)->l = And;
    ((InequProp*)(((BinProp*)P)->p1))->e1 = new VarExpr;
    ((InequProp*)(((BinProp*)P)->p1))->e2 = new IntExpr;
    ((InequProp*)(((BinProp*)P)->p1))->p = LT;
    strcpy( ((VarExpr*)(((InequProp*)(((BinProp*)P)->p1))->e1))->x, "x");
    ((IntExpr*)(((InequProp*)(((BinProp*)P)->p1))->e2))->i = 1;
    ((InequProp*)(((BinProp*)P)->p2))->e1 = new VarExpr;
    ((InequProp*)(((BinProp*)P)->p2))->e2 = new IntExpr;
    ((InequProp*)(((BinProp*)P)->p2))->p = LT;
    strcpy( ((VarExpr*)(((InequProp*)(((BinProp*)P)->p2))->e1))->x, "y");
    ((IntExpr*)(((InequProp*)(((BinProp*)P)->p2))->e2))->i = 1;
    //cfa.PrintProp(P); cout << endl;
    if(interfaceSMT(P)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //1, test BinProp Sat x=1&&y=1
    Q = new BinProp;
    ((BinProp*)Q)->p1 = new BoolProp;
    ((BinProp*)Q)->p2 = new NegProp;
    ((BinProp*)Q)->l = And;
    ((BoolProp*)((BinProp*)Q)->p1)->b = false;
    ((NegProp*)((BinProp*)Q)->p2)->p = new BinProp;
    ((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1 = new InequProp;
    ((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2 = new InequProp;
    ((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->l = And;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1))->e1 = new VarExpr;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1))->e2 = new IntExpr;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1))->p = LT;
    strcpy( ((VarExpr*)((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1))->e1)->x, "x" );
    ((IntExpr*)((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p1))->e2)->i = 1;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2))->e1 = new VarExpr;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2))->e2 = new IntExpr;
    ((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2))->p = LT;
    strcpy( ((VarExpr*)((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2))->e1)->x, "y" );
    ((IntExpr*)((InequProp*)(((BinProp*)(((NegProp*)((BinProp*)Q)->p2)->p))->p2))->e2)->i = 1;
    //cfa.PrintProp(Q); cout << endl;
    if(interfaceSMT(Q)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //2, test BinProp UNSat
    R1 = new BoolProp;
    ((BoolProp*)R1)->b = true; 
    //cfa.PrintProp(R1); cout << endl;
    if(interfaceSMT(R1)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //3.test BoolProp SAT
    R2 = new BoolProp;
    ((BoolProp*)R2)->b = false; 
    //cfa.PrintProp(R2); cout << endl;
    if(interfaceSMT(R2)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //4.test BoolProp UNSAT
    S1 = new InequProp;
    ((InequProp*)S1)->e1 = new VarExpr;
    ((InequProp*)S1)->e2 = new VarExpr;
    ((InequProp*)S1)->p = Eq;
    strcpy( ((VarExpr*)(((InequProp*)S1)->e1))->x, "x");
    strcpy( ((VarExpr*)(((InequProp*)S1)->e2))->x, "y");
    //cfa.PrintProp(S1); cout << endl;
    if(interfaceSMT(S1)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //5. test InequProp SAT
    S2 = new NegProp;
    ((NegProp*)S2)->p = new InequProp;
    ((InequProp*)(((NegProp*)S2)->p))->e1 = new VarExpr;
    ((InequProp*)(((NegProp*)S2)->p))->e2 = new VarExpr;
    ((InequProp*)(((NegProp*)S2)->p))->p = Eq;
    strcpy(((VarExpr*)(((InequProp*)(((NegProp*)S2)->p))->e1))->x, "x");
    strcpy(((VarExpr*)(((InequProp*)(((NegProp*)S2)->p))->e2))->x, "x");
    //cfa.PrintProp(S2); cout << endl;
    if(interfaceSMT(S2)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }
    //6. test NegProp UNSAT
    S3 = new NegProp;
    ((NegProp*)S3)->p = new InequProp;
    ((InequProp*)(((NegProp*)S3)->p))->e1 = new VarExpr;
    ((InequProp*)(((NegProp*)S3)->p))->e2 = new VarExpr;
    ((InequProp*)(((NegProp*)S3)->p))->p = Eq;
    strcpy(((VarExpr*)(((InequProp*)(((NegProp*)S3)->p))->e1))->x, "x");
    strcpy(((VarExpr*)(((InequProp*)(((NegProp*)S3)->p))->e2))->x, "y");
    //cfa.PrintProp(S3); cout << endl;
    if(interfaceSMT(S3)){ cout << "UNSAT!!!" << endl; }
    else{ cout << "SAT!!!" << endl; }

    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    //yicesl_read(ctx, "(define a::int)");
    //yicesl_read(ctx, "(define x1::int)");
    yicesl_read(ctx, "(define n::int)");
    yicesl_read(ctx, "(define r2::int)");
    yicesl_read(ctx, "(define r2_1::int)");
    yicesl_read(ctx, "(define i1::int)");
    //yicesl_read(ctx, "(define a'::int)");
    //yicesl_read(ctx, "(define b::int)");
    //yicesl_read(ctx, "(define y::int)");

    //yicesl_read(ctx, "(define y::int)");
    //yicesl_read(ctx, "assert( or ((set-arith-only! false)) (( not (( and (( < (x) (1) )) (( < (y) (1) )) )) )) )");
    //yicesl_read(ctx, "(set-arith-only! false)");
    //yicesl_read(ctx, "(set-evidence! false)"); //單獨也是sat
    //yicesl_read(ctx, "( assert false )");//結果是UNSAT
    //yicesl_read(ctx, "(assert true)");//結果是SAT
    //yicesl_read(ctx, "(assert( and false true))");//結果是UNSAT
    //yicesl_read(ctx, "(assert( and false (not ( and ( < x 1)  ( < y 1)))))");//結果是UNSAT
    //yicesl_read(ctx, "(assert( and false ( not (( and (( < (x) (1) )) (( < (y) (1) )) ) )) ))");//結果是SAT?
    //yicesl_read(ctx, "(assert( and false ( not ( and (( < (x) (1) )) (( < (y) (1) )) )) ))");//結果是SAT?
    //yicesl_read(ctx, "(assert( and false ( not ( and ( < (x) (1) ) ( < (y) (1) ) )) ))");//結果是SAT?
    //yicesl_read(ctx, "(assert( and false ( not ( and ( < x 1 ) ( < y 1 ) )) ))");//結果是UNSAT
    //yicesl_read(ctx, "assert( and  false  (( not (( and (( < x 1 )) (( < y 1 )) )) )) )");//結果是SAT
    //yicesl_read(ctx, "(assert not false  )");//結果是SAT?
    //yicesl_read(ctx, "assert( and ( = x 1 ) (not ( = x 1 )) )");//結果是SAT?
    //yicesl_read(ctx, "define y::bool (=> ( and ( = x 1 ) (not ( = x 1 )) ))");
    //yicesl_read(ctx, "assert( = y false)"); //,結果是SAT?
    //yicesl_read(ctx, "assert( and  false  ( not ( and ( < x 1 ) ( < y 1 ) ) ) )");//結果是SAT---X
    //yicesl_read(ctx, "( assert( and  false  ( not ( and ( < x 1 ) ( < y 1 ) ) ) ))");//結果是UNSAT
    //yicesl_read(ctx, "( assert (not true) )");//結果UN是SAT
    //yicesl_read(ctx, "( assert( not (= x x) ) )");//結果是UNSAT
    //yicesl_read(ctx, "(assert( and ( and ( and ( < 0 a ) ( < 0 b ) ) ( < b a ) ) ( not ( < 0 a ))))");//結果是SAT?
    //yicesl_read(ctx, "(assert( and ( < 0 a ) ( not ( < 0 a ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and ( and ( > a  0 ) ( > b  0 ) ) ( > a b ) ) ( not ( > a 1 ) ) ) )");//結果是UNSAT
    //yicesl_read(ctx, "( assert( and ( and ( and ( > a' 0 ) ( > b 0 ) ) ( = a ( + a' 1 ) ) ) ( not ( > a 1 ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and  true  ( = x1 1 ) ) ( not ( < x1 5 ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and  true  ( < n 20 ) ) ( not ( < 0 ( + 19 ( * -1 n ) ) ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and ( not ( > 0 ( + 2 ( * -1 x2 ) ) ) ) ( = x2 1 ) ) ( not ( < x1 10 ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( = x2 1 ) ( not ( < x1 10 ) ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and false true ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 1 ) ( = r2 ( + r2_1 1 ) ) ) ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 2 ) ) )");//結果是SAT
    yicesl_read( ctx, "( assert( and ( and ( and  true  ( not ( not ( > ( + n ( + ( * -1 i1 ) ( * -1 r2 ) ) ) -2 ) ) ) ) ( < ( - r2 1 ) ( - ( + n 1 ) i1 ) ) ) ( not ( > ( + n ( + ( * -1 i1 ) ( * -1 r2 ) ) ) -2 ) ) ) )");
    //yicesl_read(ctx, "( assert( and ( not ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 2 ) ) ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 2 ) ) )");//結果是UNSAT
    //yicesl_read(ctx, "( assert( and ( and ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 1 ) ( = r2 ( + r2_1 1 ) ) ) ( not ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 2 ) ) ) )");//結果是UNSAT
    //yicesl_read(ctx, "( assert( => ( and ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 1 ) ( = r2 ( + r2_1 1 ) ) ) ( not ( < ( + ( + r2_1 i1 ) ( * -1 n ) ) 2 ) ) )");//結果是SAT
    //yicesl_read(ctx, "( assert( and ( and  true  ( < n 20 ) ) ( > 0 ( + 19 ( * -1 n ) ) ) ) )");//結果是UNSAT
    //yicesl_read(ctx, "( assert( and ( and  true  ( < n 20 ) ) ( > 0 ( - 19 n ) ) ) )");//結果是UNSAT
    //yicesl_read(ctx, "(assert( and false ( not ( and ( < x 1 ) ( < y 1 ) ))))");//結果是UNSAT，如果沒有define那行結果會是錯
    //yicesl_read(ctx, "(assert( or false (not ( and ( < x 1)  ( < y 1)))))");//結果是SAT
    //yicesl_read(ctx, "(assert(  not ( and ( < x 1 ) ( < y 1 ) )  ))"); //也是sat?
    //yicesl_read(ctx, "(define y::int)");
    //yicesl_read(ctx, "(define T::bool (and (= x 1) (= x 2))");
    //yicesl_read(ctx, "(assert ( and (= x 1) (= x 2)))");//這行如果沒有配合上面define那行也是SAT，要配合才會是UNSAT
    //yicesl_read(ctx, "assert(( and (( < (x) (1) )) (( < (y) (1) )) ))");
    //yicesl_read(ctx, "(assert( = x 0 ))");
    //yicesl_read(ctx, "(assert( = x 2 ))");//這兩行的組合是UNSAT
    //yicesl_read(ctx, "(assert (< (x) (1)))");
    //yicesl_read(ctx, "(assert (< (y) (1)))");
    display(ctx);
    
}
